D1: From Quantified Type Theory to Modal Type Theory
A type systems assigns every expression and variable in a program a type, and throws a compile-time errors if there is a mismatch. But there is more information we can check and track at compile time, than just types; sometimes variables also have modes.
For illustration of the difference between types and modes, consider the annotation "@NonNull List<Integer> x;", here x is a variable of type list of integer, which is not null. Such an annotation is not a type but a mode. If NonNull were a type we could nest it and write "List<@NonNull Integer> x;", however this is not possible in Java.
Besides this trivial example, one in particular useful thing to use modal type theory for, is to express and check "resources". Linear type system can ensure that some values are not accidentally duplicated or destroyed, one way of manual resource management. Haskell recently added support for linear types. Quantified type theory is a particular nice way to understand the rules behind it. Here, every variable/function argument is annotated with a natural number of uses or infinity. Prime example for quantified type theory can be found in Idris.
References
The following papers are NOT directly related to each other and on varying levels of complexity, let's pick one or two of these in the first meeting, and then you find others that are related to those we picked. Ignore the others: